a(c(x1)) → a(x1)
d(a(x1)) → a(c(b(c(d(x1)))))
a(c(b(c(x1)))) → c(b(c(c(x1))))
c(x1) → b(a(a(x1)))
d(c(x1)) → a(c(d(a(x1))))
↳ QTRS
↳ DependencyPairsProof
a(c(x1)) → a(x1)
d(a(x1)) → a(c(b(c(d(x1)))))
a(c(b(c(x1)))) → c(b(c(c(x1))))
c(x1) → b(a(a(x1)))
d(c(x1)) → a(c(d(a(x1))))
D(c(x1)) → A(c(d(a(x1))))
D(c(x1)) → D(a(x1))
D(a(x1)) → C(b(c(d(x1))))
D(a(x1)) → D(x1)
D(c(x1)) → A(x1)
C(x1) → A(x1)
A(c(b(c(x1)))) → C(b(c(c(x1))))
A(c(b(c(x1)))) → C(c(x1))
A(c(x1)) → A(x1)
C(x1) → A(a(x1))
D(a(x1)) → A(c(b(c(d(x1)))))
D(c(x1)) → C(d(a(x1)))
D(a(x1)) → C(d(x1))
a(c(x1)) → a(x1)
d(a(x1)) → a(c(b(c(d(x1)))))
a(c(b(c(x1)))) → c(b(c(c(x1))))
c(x1) → b(a(a(x1)))
d(c(x1)) → a(c(d(a(x1))))
↳ QTRS
↳ DependencyPairsProof
↳ QDP
↳ DependencyGraphProof
D(c(x1)) → A(c(d(a(x1))))
D(c(x1)) → D(a(x1))
D(a(x1)) → C(b(c(d(x1))))
D(a(x1)) → D(x1)
D(c(x1)) → A(x1)
C(x1) → A(x1)
A(c(b(c(x1)))) → C(b(c(c(x1))))
A(c(b(c(x1)))) → C(c(x1))
A(c(x1)) → A(x1)
C(x1) → A(a(x1))
D(a(x1)) → A(c(b(c(d(x1)))))
D(c(x1)) → C(d(a(x1)))
D(a(x1)) → C(d(x1))
a(c(x1)) → a(x1)
d(a(x1)) → a(c(b(c(d(x1)))))
a(c(b(c(x1)))) → c(b(c(c(x1))))
c(x1) → b(a(a(x1)))
d(c(x1)) → a(c(d(a(x1))))
↳ QTRS
↳ DependencyPairsProof
↳ QDP
↳ DependencyGraphProof
↳ AND
↳ QDP
↳ QDP
C(x1) → A(x1)
A(c(b(c(x1)))) → C(c(x1))
A(c(b(c(x1)))) → C(b(c(c(x1))))
A(c(x1)) → A(x1)
C(x1) → A(a(x1))
a(c(x1)) → a(x1)
d(a(x1)) → a(c(b(c(d(x1)))))
a(c(b(c(x1)))) → c(b(c(c(x1))))
c(x1) → b(a(a(x1)))
d(c(x1)) → a(c(d(a(x1))))
↳ QTRS
↳ DependencyPairsProof
↳ QDP
↳ DependencyGraphProof
↳ AND
↳ QDP
↳ QDP
↳ QDPOrderProof
D(a(x1)) → D(x1)
D(c(x1)) → D(a(x1))
a(c(x1)) → a(x1)
d(a(x1)) → a(c(b(c(d(x1)))))
a(c(b(c(x1)))) → c(b(c(c(x1))))
c(x1) → b(a(a(x1)))
d(c(x1)) → a(c(d(a(x1))))
The following pairs can be oriented strictly and are deleted.
The remaining pairs can at least be oriented weakly.
D(c(x1)) → D(a(x1))
Used ordering: Polynomial interpretation [25,35]:
D(a(x1)) → D(x1)
The value of delta used in the strict ordering is 3.
POL(c(x1)) = 3 + (5/4)x_1
POL(D(x1)) = x_1
POL(a(x1)) = (5/4)x_1
POL(b(x1)) = 1/4
c(x1) → b(a(a(x1)))
a(c(b(c(x1)))) → c(b(c(c(x1))))
a(c(x1)) → a(x1)
↳ QTRS
↳ DependencyPairsProof
↳ QDP
↳ DependencyGraphProof
↳ AND
↳ QDP
↳ QDP
↳ QDPOrderProof
↳ QDP
↳ QDPOrderProof
D(a(x1)) → D(x1)
a(c(x1)) → a(x1)
d(a(x1)) → a(c(b(c(d(x1)))))
a(c(b(c(x1)))) → c(b(c(c(x1))))
c(x1) → b(a(a(x1)))
d(c(x1)) → a(c(d(a(x1))))
The following pairs can be oriented strictly and are deleted.
The remaining pairs can at least be oriented weakly.
D(a(x1)) → D(x1)
The value of delta used in the strict ordering is 1/2.
POL(D(x1)) = (2)x_1
POL(a(x1)) = 1/4 + (7/2)x_1
↳ QTRS
↳ DependencyPairsProof
↳ QDP
↳ DependencyGraphProof
↳ AND
↳ QDP
↳ QDP
↳ QDPOrderProof
↳ QDP
↳ QDPOrderProof
↳ QDP
↳ PisEmptyProof
a(c(x1)) → a(x1)
d(a(x1)) → a(c(b(c(d(x1)))))
a(c(b(c(x1)))) → c(b(c(c(x1))))
c(x1) → b(a(a(x1)))
d(c(x1)) → a(c(d(a(x1))))